| Definitions | t  T, "$x", Id, <a,b>, lnk$n{$a to $b}, IdLnk,  x:A. B(x), source(l), loc(e), s = t, E, {x:A| B(x) }, x:A  B(x), es-init(es;e), False, P   Q,  A, Knd, Prop, kind(e),  x.A(x), left+right, x:A B(x), ES, Type, P & Q, es-decls(es;i;ds;da), A & B, es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)), True, A/x,y. B(x;y), 1of(t),  x. t(x), e[e1,e2].P(e),  T, , P  Q, P Q, e  e' , P  Q, Dec(P), e[e1,e2).P(e), e2 = first e  e1.P(e), x,y. t(x;y), [e1,e2]~([a,b].p(a;b))+, [e, e'], (x l),  x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), i=j, i<j, ij, s-insert(x;l), ecl ind eclbase compseq tag def, ecl ind eclact compseq tag def, ecl ind eclthrow compseq tag def, xL.P(x), ecl-ex(x), ecl ind eclor compseq tag def,  b, ecl-es-halt(es;x), Void,  x:A. B(x), Top, rcv(l,tg), KindDeq, ecl ind eclrepeat compseq tag def, ecl-es-act(es;m;x), State(ds), x : v, Valtype(da;k), #$n, AB, a<b,  ,  , true, eclbase(k;test), eclthrow(a;n), a.n, eclor(a;b), [a]*, @i[[x;snd;upd]], 2of(t), EqDecider(T), IdDeq, f(x)?z, type List, a:A fp B(a), update-spec(ds;da), k sends on l with tag tg [s,v.f(s;v)], at marker n, update-spec-decl(upd;ds), msg-spec-loc(snd;i) |
